es:ES, i, x:Id, T:Type, P:(T), Lx:(Knd List).
@i only Lx affect x:T
 @i(x:T)
 e@i. (kind(e)  Lx)  P(x when e)  P((x after e))
 @i stable state.P(state.x)   

latex

Definitions

t  T, P  Q, x:A. B(x), x when e, (x after e), <a, b>, s = t, x(s), f(a), left + right, P  Q, Dec(P), e@i. P(e), vartype(i;x), x:A  B(x), P & Q, @i(x:T), {T}, SQType(T), Id, , s ~ t, Atom$n, let x,y = A in B(x;y), t.1, E, x:AB(x), loc(e), False, A, b, b, , discrete(i;x), P  Q, Unit, (discrete state after e), (discrete state when e), @i stable state.P(state)  , s.x, {x:A| B(x)} , A c B, @i only L affect x:T, ES, Type, type List, x. t(x), Knd, kind(e), (x  l)

Lemmas

alle-at wf, l member wf, es-dtype wf, es-frame wf, event system wf, es-after wf, es-E wf, es-loc wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-isconst wf, bool wf, bnot wf, not wf, assert wf, es-when wf, Id wf, Id sq, es-vartype wf, decidable l member, decidable equal Kind, es-kind wf, Knd wf